//
// THIS FILE IS AUTOMATICALLY GENERATED!!
//
// Generated at Thu 06-Dec-2012 by the VDM++ to JAVA Code Generator
// (v8.0 - Mon 09-Jul-2007 09:32:40)
//
// Supported compilers:
// jdk1.4
//

// ***** VDMTOOLS START Name=HeaderComment KEEP=NO
// ***** VDMTOOLS END Name=HeaderComment

// ***** VDMTOOLS START Name=package KEEP=NO
// ***** VDMTOOLS END Name=package

// ***** VDMTOOLS START Name=imports KEEP=NO

import jp.co.csk.vdm.toolbox.VDM.*;
import java.util.*;
import jp.co.csk.vdm.toolbox.VDM.jdk.*;
// ***** VDMTOOLS END Name=imports



public class State implements EvaluatePP {

// ***** VDMTOOLS START Name=vdmComp KEEP=NO
  static UTIL.VDMCompare vdmComp = new UTIL.VDMCompare();
// ***** VDMTOOLS END Name=vdmComp

// ***** VDMTOOLS START Name=name KEEP=NO
  private volatile String name = null;
// ***** VDMTOOLS END Name=name

// ***** VDMTOOLS START Name=transitions KEEP=NO
  private volatile Vector transitions = null;
// ***** VDMTOOLS END Name=transitions

// ***** VDMTOOLS START Name=sentinel KEEP=NO
  volatile Sentinel sentinel;
// ***** VDMTOOLS END Name=sentinel


// ***** VDMTOOLS START Name=StateSentinel KEEP=NO
  class StateSentinel extends Sentinel {

    public final int State = 0;

    public final int getName = 1;

    public final int isDeadEnd = 2;

    public final int search_u_u1_uI = 3;

    public final int addTransition = 4;

    public final int isUniqueTransitionValue = 5;

    public final int search_u_u3_us_un_uState_ut_us_un_uState_uI = 6;

    public final int nr_functions = 7;


    public StateSentinel () throws CGException {}


    public StateSentinel (EvaluatePP instance) throws CGException {
      init(nr_functions, instance);
    }

  }
// ***** VDMTOOLS END Name=StateSentinel
;

// ***** VDMTOOLS START Name=evaluatePP KEEP=NO
  public Boolean evaluatePP (int fnr) throws CGException {
    return new Boolean(true);
  }
// ***** VDMTOOLS END Name=evaluatePP


// ***** VDMTOOLS START Name=setSentinel KEEP=NO
  public void setSentinel () {
    try {
      sentinel = new StateSentinel(this);
    }
    catch (CGException e) {
      System.out.println(e.getMessage());
    }
  }
// ***** VDMTOOLS END Name=setSentinel


// ***** VDMTOOLS START Name=State KEEP=NO
  public State () throws CGException {
    try {

      setSentinel();
      transitions = new Vector();
    }
    catch (Exception e){

      e.printStackTrace(System.out);
      System.out.println(e.getMessage());
    }
  }
// ***** VDMTOOLS END Name=State


// ***** VDMTOOLS START Name=State KEEP=NO
  public State (final String n) throws CGException {

    try {

      setSentinel();
      transitions = new Vector();
    }
    catch (Exception e){

      e.printStackTrace(System.out);
      System.out.println(e.getMessage());
    }
    name = UTIL.ConvertToString(UTIL.clone(n));
  }
// ***** VDMTOOLS END Name=State


// ***** VDMTOOLS START Name=addTransition KEEP=NO
  public void addTransition (final Transition t) throws CGException {

    if (!this.pre_addTransition(t).booleanValue()) 
      UTIL.RunTime("Run-Time Error:Precondition failure in addTransition");
    sentinel.entering(((StateSentinel) sentinel).addTransition);
    try {
      transitions.add(t);
    }
    finally {
      sentinel.leaving(((StateSentinel) sentinel).addTransition);
    }
  }
// ***** VDMTOOLS END Name=addTransition


// ***** VDMTOOLS START Name=pre_addTransition KEEP=NO
  public Boolean pre_addTransition (final Transition t) throws CGException {

    Boolean varRes_2 = null;
    Boolean var1_3 = null;
    Boolean var1_4 = null;
    State var1_5 = null;
    var1_5 = (State) t.getStartState();
    var1_4 = new Boolean(UTIL.equals(var1_5, this));
    {
      if ((var1_3 = var1_4).booleanValue()) {

        Boolean var2_7 = null;
        HashSet var2_9 = new HashSet();
        HashSet set_11 = new HashSet();
        Enumeration enm_12 = transitions.elements();
        while ( enm_12.hasMoreElements())
          set_11.add(enm_12.nextElement());
        var2_9 = set_11;
        var2_7 = new Boolean(!var2_9.contains(t));
        var1_3 = var2_7;
      }
    }
    {
      if ((varRes_2 = var1_3).booleanValue()) 
        varRes_2 = isUniqueTransitionValue((Transition) t);
    }
    return varRes_2;
  }
// ***** VDMTOOLS END Name=pre_addTransition


// ***** VDMTOOLS START Name=getName KEEP=NO
  public String getName () throws CGException {

    sentinel.entering(((StateSentinel) sentinel).getName);
    try {
      return name;
    }
    finally {
      sentinel.leaving(((StateSentinel) sentinel).getName);
    }
  }
// ***** VDMTOOLS END Name=getName


// ***** VDMTOOLS START Name=isUniqueTransitionValue KEEP=NO
  public Boolean isUniqueTransitionValue (final Transition t) throws CGException {

    if (!this.pre_isUniqueTransitionValue(t).booleanValue()) 
      UTIL.RunTime("Run-Time Error:Precondition failure in isUniqueTransitionValue");
    sentinel.entering(((StateSentinel) sentinel).isUniqueTransitionValue);
    try {
      return new Boolean(true);
    }
    finally {
      sentinel.leaving(((StateSentinel) sentinel).isUniqueTransitionValue);
    }
  }
// ***** VDMTOOLS END Name=isUniqueTransitionValue


// ***** VDMTOOLS START Name=pre_isUniqueTransitionValue KEEP=NO
  public Boolean pre_isUniqueTransitionValue (final Transition t) throws CGException {

    Boolean varRes_2 = null;
    boolean tmpQuant_3 = true;
    {

      HashSet e1_set_9 = new HashSet(transitions);
      Transition transition = null;
      {
        for (Iterator enm_11 = e1_set_9.iterator(); enm_11.hasNext() && tmpQuant_3; ) {

          Transition elem_10 = (Transition) enm_11.next();
          transition = (Transition) elem_10;
          Boolean pred_4 = null;
          String var1_5 = null;
          var1_5 = transition.getName();
          String var2_6 = null;
          var2_6 = t.getName();
          pred_4 = new Boolean(!UTIL.equals(var1_5, var2_6));
          if (pred_4.booleanValue()) {}
          else 
            tmpQuant_3 = false;
        }
      }
    }
    varRes_2 = new Boolean(tmpQuant_3);
    return varRes_2;
  }
// ***** VDMTOOLS END Name=pre_isUniqueTransitionValue


// ***** VDMTOOLS START Name=isDeadEnd KEEP=NO
  public Boolean isDeadEnd () throws CGException {

    sentinel.entering(((StateSentinel) sentinel).isDeadEnd);
    try {
      return new Boolean(UTIL.equals(transitions, new Vector()));
    }
    finally {
      sentinel.leaving(((StateSentinel) sentinel).isDeadEnd);
    }
  }
// ***** VDMTOOLS END Name=isDeadEnd


// ***** VDMTOOLS START Name=search KEEP=NO
  public HashSet search (final Integer n) throws CGException {

    sentinel.entering(((StateSentinel) sentinel).search_u_u1_uI);
    try {

      HashSet rexpr_2 = new HashSet();
      Vector par_5 = null;
      par_5 = new Vector();
      par_5.add(this);
      {

        Vector par_7 = null;
        par_7 = new Vector();
        par_7.add(this);
        rexpr_2 = (HashSet) search(par_7, new HashSet(), n);
      }
      return rexpr_2;
    }
    finally {
      sentinel.leaving(((StateSentinel) sentinel).search_u_u1_uI);
    }
  }
// ***** VDMTOOLS END Name=search


// ***** VDMTOOLS START Name=search KEEP=NO
  public HashSet search (final Vector tseq, final HashSet aseqs, final Integer n) throws CGException {

    if (!this.pre_search(tseq, aseqs, n).booleanValue()) 
      UTIL.RunTime("Run-Time Error:Precondition failure in search");
    sentinel.entering(((StateSentinel) sentinel).search_u_u3_us_un_uState_ut_us_un_uState_uI);
    try {
      if (isDeadEnd().booleanValue()) 
        return new HashSet();
      else {

        Vector to_uvisit = transitions;
        Vector thisSeq = tseq;
        HashSet allSeqs = aseqs;
        Integer tmp_un = new Integer(n.intValue() - new Integer(1).intValue());
        while ( true){

          Boolean whCrtl_7 = null;
          {
            if ((whCrtl_7 = new Boolean(!UTIL.equals(to_uvisit, new Vector()))).booleanValue()) 
              whCrtl_7 = new Boolean(!(tmp_un.intValue() == new Integer(0).intValue()));
          }
          if (whCrtl_7.booleanValue()) {

            State curr_ustate = null;
            Transition obj_16 = null;
            obj_16 = (Transition) (Transition) to_uvisit.get(0);
            curr_ustate = (State) obj_16.getEndState();
            {

              to_uvisit = (Vector) UTIL.ConvertToList(UTIL.clone(new Vector(to_uvisit.subList(1, to_uvisit.size()))));
              HashSet rhs_20 = new HashSet();
              HashSet var1_21 = new HashSet();
              HashSet var2_23 = new HashSet();
              Vector enum_set_24 = null;
              Vector var2_26 = null;
              var2_26 = new Vector();
              var2_26.add(curr_ustate);
              enum_set_24 = (Vector) thisSeq.clone();
              enum_set_24.addAll(var2_26);
              var2_23 = new HashSet();
              var2_23.add(enum_set_24);
              var1_21 = (HashSet) allSeqs.clone();
              var1_21.addAll(var2_23);
              HashSet var2_28 = new HashSet();
              Object tmpGen_29 = null;
              Vector par_32 = null;
              Vector var2_34 = null;
              var2_34 = new Vector();
              var2_34.add(curr_ustate);
              par_32 = (Vector) thisSeq.clone();
              par_32.addAll(var2_34);
              {

                Vector par_36 = null;
                Vector var2_38 = null;
                var2_38 = new Vector();
                var2_38.add(curr_ustate);
                par_36 = (Vector) thisSeq.clone();
                par_36.addAll(var2_38);
                var2_28 = (HashSet) curr_ustate.search(par_36, allSeqs, tmp_un);
              }
              rhs_20 = (HashSet) var1_21.clone();
              rhs_20.addAll(var2_28);
              allSeqs = (HashSet) UTIL.clone(rhs_20);
            }
          }
          else 
            break;
        }
        return allSeqs;
      }
    }
    finally {
      sentinel.leaving(((StateSentinel) sentinel).search_u_u3_us_un_uState_ut_us_un_uState_uI);
    }
  }
// ***** VDMTOOLS END Name=search


// ***** VDMTOOLS START Name=pre_search KEEP=NO
  public Boolean pre_search (final Vector tseq, final HashSet aseqs, final Integer n) throws CGException {

    Boolean varRes_4 = null;
    {
      if ((varRes_4 = new Boolean((new Integer(tseq.size()).intValue()) > (new Integer(0).intValue()))).booleanValue()) 
        varRes_4 = new Boolean((n.intValue()) >= (new Integer(0).intValue()));
    }
    return varRes_4;
  }
// ***** VDMTOOLS END Name=pre_search

}
;
